Please only leave one newline between each theorem.

This is now more general than the above, so we should have

/-- Substitution of a locally closed term respects a single reduction step. -/
lemma redex_subst_cong_lc (s s' t : Term Var) (x : Var) (step : s ⭢βᶠ s') (h_lc : LC t) :
    s [ x := t ] ⭢βᶠ s' [ x := t ] := ... -- proof omitted

/-- Substitution respects a single reduction step of a free variable. -/
lemma redex_subst_cong (s s' : Term Var) (x y : Var) (step : s ⭢βᶠ s') :
    s [ x := fvar y ] ⭢βᶠ s' [ x := fvar y ] := by
  grind [redex_subst_cong_lc]

Please note that I tweaked the docstrings a bit.

(The redex_subst_cong name should probably change, but these earliest modules have bad naming in general so I'll come back and do that myself.)

I'm not sure I'd add this as a theorem, because it is exactly the definition of the constructor. Anywhere (like below in steps_open_l_abs) you would use this, you can just do cases on the M.abs ⭢βᶠ M'.abs and get the same result.

You are right.

A better name without a number?

steps_subst_cong_r? I was not sure how to name many of these, I did not yet figure out the naming algorithm behind the existing lemmas.

This seems fine. (As I think I mentioned elsewhere I need to overhaul the naming for these modules, so any difficultly picking names is probably my fault!)

Please use named hypotheses here.